Nuprl Lemma : agree_on_equiv
4,23
postcript
pdf
T
:Type,
P
:(
T
Prop). EquivRel
_1
,
_2
:
T
List.
_1
agree_on(
T
;
a
.
P
(
a
))
_2
latex
Definitions
t
T
,
||
as
||
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
P
Q
,
A
&
B
,
Prop
,
l
[
i
]
,
x
(
s
)
,
x
f
y
,
Trans
x
,
y
:
T
.
E
(
x
;
y
)
,
Sym
x
,
y
:
T
.
E
(
x
;
y
)
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
EquivRel
x
,
y
:
T
.
E
(
x
;
y
)
,
agree_on(
T
;
x
.
P
(
x
))
,
True
,
{
T
}
Lemmas
le
wf
,
length
wf1
,
int
seg
wf
,
select
wf
origin
T:Type, P:(T
Prop). EquivRel _1,_2:T List. _1 agree_on(T;a.P(a)) _2 T:Type, P:(TProp). EquivRel _1,_2:T List. _1 agree_on(T;a.P(a)) _2 
T
Q
A
B j < k
}x:A. B(x)
Q